YES 3.193
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => Either a b -> [Either a b] -> [Int]) :: (Eq b, Eq a) => Either a b -> [Either a b] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (\vv1 ->
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\vv1→
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices0 | p vv1 | =
case | vv1 of | | (x,i) | → if p x then i : [] else [] |
| _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => Either a b -> [Either a b] -> [Int]) :: (Eq a, Eq b) => Either a b -> [Either a b] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = |
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Case Reductions:
The following Case expression
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices00 | p (x,i) | = if p x then i : [] else [] |
findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => Either b a -> [Either b a] -> [Int]) :: (Eq a, Eq b) => Either b a -> [Either b a] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | if p x then i : [] else [] |
findIndices00 | p _ | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
findIndices000 | i True | = i : [] |
findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => Either a b -> [Either a b] -> [Int]) :: (Eq a, Eq b) => Either a b -> [Either a b] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p _ | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((elemIndices :: (Eq a, Eq b) => Either a b -> [Either a b] -> [Int]) :: (Eq a, Eq b) => Either a b -> [Either a b] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule List
| ((elemIndices :: (Eq a, Eq b) => Either b a -> [Either b a] -> [Int]) :: (Eq a, Eq b) => Either b a -> [Either b a] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule List
| (elemIndices :: (Eq a, Eq b) => Either a b -> [Either a b] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yu7100), Succ(yu411000000)) → new_primPlusNat(yu7100, yu411000000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yu7100), Succ(yu411000000)) → new_primPlusNat(yu7100, yu411000000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yu30000), Succ(yu41100000)) → new_primMulNat(yu30000, Succ(yu41100000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yu30000), Succ(yu41100000)) → new_primMulNat(yu30000, Succ(yu41100000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_Maybe, bbh)), bbb), gc) → new_esEs2(yu300, yu411000, bbh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_Either, db), dc)) → new_esEs1(yu302, yu411002, db, dc)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_[], bb)), gc) → new_esEs(yu300, yu411000, bb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, fh), cd, dh) → new_esEs2(yu300, yu411000, fh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_Maybe, dd)) → new_esEs2(yu302, yu411002, dd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_@2, ga), gb)), cd), dh), gc) → new_esEs3(yu300, yu411000, ga, gb)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(yu30, yu41100, bce, bcf, bcg)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_@2, he), hf)), gc) → new_esEs3(yu300, yu411000, he, hf)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], bba), bbb) → new_esEs(yu300, yu411000, bba)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, bbc), bbd), bbe), bbb) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
new_esEs1(Left(yu30), Left(yu41100), app(app(ty_Either, gd), ge), gc) → new_esEs1(yu30, yu41100, gd, ge)
new_esEs2(Just(yu300), Just(yu411000), app(ty_Maybe, hd)) → new_esEs2(yu300, yu411000, hd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_[], ce)) → new_esEs(yu302, yu411002, ce)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_Either, ed), ee), dh) → new_esEs1(yu301, yu411001, ed, ee)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(app(ty_@3, baa), bab), bac)), gc) → new_esEs0(yu301, yu411001, baa, bab, bac)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_[], hh)) → new_esEs(yu301, yu411001, hh)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(app(ty_@3, gg), gh), ha)), gc) → new_esEs0(yu300, yu411000, gg, gh, ha)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_[], hh)), gc) → new_esEs(yu301, yu411001, hh)
new_esEs2(Just(yu300), Just(yu411000), app(app(app(ty_@3, gg), gh), ha)) → new_esEs0(yu300, yu411000, gg, gh, ha)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(yu300, yu411000, ga, gb)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(app(ty_@3, bbc), bbd), bbe)), bbb), gc) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_Either, ff), fg)), cd), dh), gc) → new_esEs1(yu300, yu411000, ff, fg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_[], dg), dh) → new_esEs(yu301, yu411001, dg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_Maybe, dd)), gc) → new_esEs2(yu302, yu411002, dd)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bca), bcb), bbb) → new_esEs3(yu300, yu411000, bca, bcb)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_@2, bca), bcb)), bbb), gc) → new_esEs3(yu300, yu411000, bca, bcb)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_@2, ca), cb)), gc) → new_esEs3(yu300, yu411000, ca, cb)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_@2, eg), eh)), dh), gc) → new_esEs3(yu301, yu411001, eg, eh)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(app(ty_@3, baa), bab), bac)) → new_esEs0(yu301, yu411001, baa, bab, bac)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_[], bcd)) → new_esEs(yu30, yu41100, bcd)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_[], gf)), gc) → new_esEs(yu300, yu411000, gf)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_Maybe, hd)), gc) → new_esEs2(yu300, yu411000, hd)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_Maybe, bdb)) → new_esEs2(yu30, yu41100, bdb)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_Either, db), dc)), gc) → new_esEs1(yu302, yu411002, db, dc)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_@2, bag), bah)), gc) → new_esEs3(yu301, yu411001, bag, bah)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(yu302, yu411002, de, df)
new_esEs2(Just(yu300), Just(yu411000), app(ty_[], gf)) → new_esEs(yu300, yu411000, gf)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bbf), bbg), bbb) → new_esEs1(yu300, yu411000, bbf, bbg)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_Maybe, baf)) → new_esEs2(yu301, yu411001, baf)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_[], fa)), cd), dh), gc) → new_esEs(yu300, yu411000, fa)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, ff), fg), cd, dh) → new_esEs1(yu300, yu411000, ff, fg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(app(ty_@3, fb), fc), fd)), cd), dh), gc) → new_esEs0(yu300, yu411000, fb, fc, fd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_@2, de), df)), gc) → new_esEs3(yu302, yu411002, de, df)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], ba), gc) → new_esEs(yu301, yu411001, ba)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_Either, bad), bae)), gc) → new_esEs1(yu301, yu411001, bad, bae)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_Either, ed), ee)), dh), gc) → new_esEs1(yu301, yu411001, ed, ee)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_[], dg)), dh), gc) → new_esEs(yu301, yu411001, dg)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_Either, bch), bda)) → new_esEs1(yu30, yu41100, bch, bda)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(yu301, yu411001, ea, eb, ec)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_[], bba)), bbb), gc) → new_esEs(yu300, yu411000, bba)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, bh)) → new_esEs2(yu300, yu411000, bh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(yu301, yu411001, eg, eh)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(app(ty_@3, bc), bd), be)), gc) → new_esEs0(yu300, yu411000, bc, bd, be)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(app(ty_@3, ea), eb), ec)), dh), gc) → new_esEs0(yu301, yu411001, ea, eb, ec)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_@2, bag), bah)) → new_esEs3(yu301, yu411001, bag, bah)
new_esEs2(Just(yu300), Just(yu411000), app(app(ty_Either, hb), hc)) → new_esEs1(yu300, yu411000, hb, hc)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], fa), cd, dh) → new_esEs(yu300, yu411000, fa)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), ba) → new_esEs(yu301, yu411001, ba)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, bbh), bbb) → new_esEs2(yu300, yu411000, bbh)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_Either, bad), bae)) → new_esEs1(yu301, yu411001, bad, bae)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(yu302, yu411002, cf, cg, da)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_Either, bbf), bbg)), bbb), gc) → new_esEs1(yu300, yu411000, bbf, bbg)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_Either, hb), hc)), gc) → new_esEs1(yu300, yu411000, hb, hc)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(app(ty_@3, cf), cg), da)), gc) → new_esEs0(yu302, yu411002, cf, cg, da)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_Maybe, bh)), gc) → new_esEs2(yu300, yu411000, bh)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_Maybe, baf)), gc) → new_esEs2(yu301, yu411001, baf)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(yu300, yu411000, bc, bd, be)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_Either, bf), bg)), gc) → new_esEs1(yu300, yu411000, bf, bg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_Maybe, fh)), cd), dh), gc) → new_esEs2(yu300, yu411000, fh)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_[], ce)), gc) → new_esEs(yu302, yu411002, ce)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, ca), cb)) → new_esEs3(yu300, yu411000, ca, cb)
new_esEs2(Just(yu300), Just(yu411000), app(app(ty_@2, he), hf)) → new_esEs3(yu300, yu411000, he, hf)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, bf), bg)) → new_esEs1(yu300, yu411000, bf, bg)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(yu30, yu41100, bdc, bdd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_Maybe, ef)), dh), gc) → new_esEs2(yu301, yu411001, ef)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_Maybe, ef), dh) → new_esEs2(yu301, yu411001, ef)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], bb)) → new_esEs(yu300, yu411000, bb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(yu300, yu411000, fb, fc, fd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(yu300), Just(yu411000), app(app(ty_Either, hb), hc)) → new_esEs1(yu300, yu411000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(yu300), Just(yu411000), app(app(app(ty_@3, gg), gh), ha)) → new_esEs0(yu300, yu411000, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, bf), bg)) → new_esEs1(yu300, yu411000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(yu300, yu411000, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(yu300), Just(yu411000), app(app(ty_@2, he), hf)) → new_esEs3(yu300, yu411000, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, ca), cb)) → new_esEs3(yu300, yu411000, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(yu300), Just(yu411000), app(ty_Maybe, hd)) → new_esEs2(yu300, yu411000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(yu300), Just(yu411000), app(ty_[], gf)) → new_esEs(yu300, yu411000, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, bh)) → new_esEs2(yu300, yu411000, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(yu30), Left(yu41100), app(app(ty_Either, gd), ge), gc) → new_esEs1(yu30, yu41100, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_Either, ff), fg)), cd), dh), gc) → new_esEs1(yu300, yu411000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_Either, db), dc)), gc) → new_esEs1(yu302, yu411002, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_Either, bad), bae)), gc) → new_esEs1(yu301, yu411001, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_Either, ed), ee)), dh), gc) → new_esEs1(yu301, yu411001, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_Either, bch), bda)) → new_esEs1(yu30, yu41100, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_Either, bbf), bbg)), bbb), gc) → new_esEs1(yu300, yu411000, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_Either, hb), hc)), gc) → new_esEs1(yu300, yu411000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_Either, bf), bg)), gc) → new_esEs1(yu300, yu411000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bbf), bbg), bbb) → new_esEs1(yu300, yu411000, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_Either, bad), bae)) → new_esEs1(yu301, yu411001, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_Either, db), dc)) → new_esEs1(yu302, yu411002, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_Either, ed), ee), dh) → new_esEs1(yu301, yu411001, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, ff), fg), cd, dh) → new_esEs1(yu300, yu411000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(yu30, yu41100, bce, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(app(ty_@3, baa), bab), bac)), gc) → new_esEs0(yu301, yu411001, baa, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(app(ty_@3, gg), gh), ha)), gc) → new_esEs0(yu300, yu411000, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(app(ty_@3, bbc), bbd), bbe)), bbb), gc) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(app(ty_@3, fb), fc), fd)), cd), dh), gc) → new_esEs0(yu300, yu411000, fb, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(app(ty_@3, bc), bd), be)), gc) → new_esEs0(yu300, yu411000, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(app(ty_@3, ea), eb), ec)), dh), gc) → new_esEs0(yu301, yu411001, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(app(ty_@3, cf), cg), da)), gc) → new_esEs0(yu302, yu411002, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_@2, ga), gb)), cd), dh), gc) → new_esEs3(yu300, yu411000, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_@2, he), hf)), gc) → new_esEs3(yu300, yu411000, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_@2, bca), bcb)), bbb), gc) → new_esEs3(yu300, yu411000, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_@2, ca), cb)), gc) → new_esEs3(yu300, yu411000, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_@2, eg), eh)), dh), gc) → new_esEs3(yu301, yu411001, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_@2, bag), bah)), gc) → new_esEs3(yu301, yu411001, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_@2, de), df)), gc) → new_esEs3(yu302, yu411002, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(yu30, yu41100, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_Maybe, bbh)), bbb), gc) → new_esEs2(yu300, yu411000, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_Maybe, dd)), gc) → new_esEs2(yu302, yu411002, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_Maybe, hd)), gc) → new_esEs2(yu300, yu411000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_Maybe, bdb)) → new_esEs2(yu30, yu41100, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_Maybe, bh)), gc) → new_esEs2(yu300, yu411000, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_Maybe, baf)), gc) → new_esEs2(yu301, yu411001, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_Maybe, fh)), cd), dh), gc) → new_esEs2(yu300, yu411000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_Maybe, ef)), dh), gc) → new_esEs2(yu301, yu411001, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_[], bb)), gc) → new_esEs(yu300, yu411000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_[], hh)), gc) → new_esEs(yu301, yu411001, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_[], bcd)) → new_esEs(yu30, yu41100, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_[], gf)), gc) → new_esEs(yu300, yu411000, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_[], fa)), cd), dh), gc) → new_esEs(yu300, yu411000, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], ba), gc) → new_esEs(yu301, yu411001, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_[], dg)), dh), gc) → new_esEs(yu301, yu411001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_[], bba)), bbb), gc) → new_esEs(yu300, yu411000, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_[], ce)), gc) → new_esEs(yu302, yu411002, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, bbc), bbd), bbe), bbb) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(app(ty_@3, baa), bab), bac)) → new_esEs0(yu301, yu411001, baa, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(yu301, yu411001, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(yu302, yu411002, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(yu300, yu411000, fb, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), ba) → new_esEs(yu301, yu411001, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], bb)) → new_esEs(yu300, yu411000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bca), bcb), bbb) → new_esEs3(yu300, yu411000, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_@2, bag), bah)) → new_esEs3(yu301, yu411001, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_Maybe, baf)) → new_esEs2(yu301, yu411001, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, bbh), bbb) → new_esEs2(yu300, yu411000, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], bba), bbb) → new_esEs(yu300, yu411000, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_[], hh)) → new_esEs(yu301, yu411001, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(yu300, yu411000, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(yu302, yu411002, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(yu301, yu411001, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, fh), cd, dh) → new_esEs2(yu300, yu411000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_Maybe, dd)) → new_esEs2(yu302, yu411002, dd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_Maybe, ef), dh) → new_esEs2(yu301, yu411001, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_[], ce)) → new_esEs(yu302, yu411002, ce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_[], dg), dh) → new_esEs(yu301, yu411001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], fa), cd, dh) → new_esEs(yu300, yu411000, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(yu3, :(yu4110, yu4111), yu64, ba, bb) → new_foldr(yu3, yu4111, new_primPlusNat0(yu64, Zero), ba, bb)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, yu41100000) → Succ(yu41100000)
new_primPlusNat0(Succ(yu710), yu41100000) → Succ(Succ(new_primPlusNat1(yu710, yu41100000)))
new_primPlusNat1(Succ(yu7100), Zero) → Succ(yu7100)
new_primPlusNat1(Zero, Succ(yu411000000)) → Succ(yu411000000)
new_primPlusNat1(Succ(yu7100), Succ(yu411000000)) → Succ(Succ(new_primPlusNat1(yu7100, yu411000000)))
new_primPlusNat1(Zero, Zero) → Zero
The set Q consists of the following terms:
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(yu3, :(yu4110, yu4111), yu64, ba, bb) → new_foldr(yu3, yu4111, new_primPlusNat0(yu64, Zero), ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 4 >= 4, 5 >= 5